i:Id, a:Atom1, k:Knd, A:MsgA.
AtomFree(ds(A))
 AtomFree(da(A))
 z,z@0. filter(m.source(mlnk(m)) = i;A.sends(k,z,z@0)):A.stateA.da(k)
 ({m:Msg(l,tg. A.dout(l,tg))| source(mlnk(m)) = i } List)>>a
 ma-body(A):Shape(A)>>a 

latex

Definitions

x:A. B(x), P  Q, t  T, mlnk(m), 1of(t), S  T, Msg(M), x. t(x), Prop, 2of(t), P  Q, P & Q, P  Q, SQType(T), {T}, x,y. t(x;y), Shape(M), ma-body(M), MsgA(ds;da), ds(M), da(M), Valtype(da;k), P  Q, M.Msg, Msg(da), x(s), MsgA, M.state, M.da(a), M.dout(l,tg), M.sends(k,s,v), x(s1,s2), False, AtomFree(d)

Lemmas

atom-free-ma-state, atom-free-ma-da, atom-free-ma-msg-from, atom-free-decl wf, Kind-deq wf, ma da wf, Id wf, id-deq wf, ma ds wf, msga wf, Knd wf, filter type, ma-msg wf, eq id wf, lsrc wf, ma-send-val wf, Msg wf, ma-dout wf, IdLnk wf, mlnk wf, assert wf, ma-da wf, assert-eq-id, pi1 wf, atom-free-fpf, atom-free-Id, atom-free-Knd, inherence-ap-elim, fpf wf, ma-state wf, fpf-cap wf, top wf, rcv wf, pi2 wf, concat wf, map wf, deq property, Knd sq, tagged-messages wf, subtype rel list, atom-free-function, atom-free-list, inherence-trivial, pair-inherence, locl wf, inheres wf